M:MsgA, x:Id, v:M.ds(x). M.init(x,v)  Prop 

latex

Definitions	False, Unit, P  Q, P & Q, , b, A, MsgA, M.ds(x), M.init(x,v), z != f(x)  P(a;z), b, x  dom(f), Prop, f(x), P  Q, a:A fp B(a), f(x)?z, x. t(x), x:A. B(x), IdDeq, Top, t  T, Id
Lemmas	Id wf, top wf, id-deq wf, fpf-cap wf, fpf-trivial-subtype-top, fpf-ap wf, fpf-dom wf, assert wf, msga wf, not wf, bnot wf, subtype rel self, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert